In recent years, formal methods have undergone a fast development. The authors give a brief review on the formal methods used in software and hardware verification. The main thread of the analysis consists of descriptions of logical systems and their related verification techniques and tools. The purpose is to help engineers to select formal tools and apply them to their work. This paper starts with a review of automated proving techniques based on propositional logic and temporal logic, including SAT, BDD, model checking, and SMT. For first order logic based theorem provers, the authors discuss ACL2, VDM method and B method. Among proof assistants which are based on higher order logics, the authors pick HOL, PVS and COQ. Advancements in commercial formal verification tools are discussed.

Different views of software architecture in UML diagrams are presented. It shows how UML can be used to model different aspects of software architecture. The semantics of UML diagrams are expressed in the notation of Communication Sequential Process(CSP). Different view models of software architectures are linked together based on the CSP semantics. The issue of refining such architectural specifications is also discussed, where software architectures can be refined in a manner that preserves desired system properties.

It is described that a practical application of the algorithm of Group Signatures in Access Control System(ACS). The first part includes an introduction on the concepts of Group Signature and ACS, and an analysis of the weakness of current ACS; then there is a description of the proposed model of access control system based on group signatures. In this description, the system, the format definition, the flow description and the characters of it are described, including an analysis on its virtue and weakness.

An algorithm for generating 3D surface of functions defined implicitly by algebraic equations is given. Tetrahedron division of the space is used in the algorithm. The approximate surface of functions is formed by pieces which are obtained from each of the tetrahedrons. This algorithm is relatively ease to implement and very practical. The algorithm can also be used to generating contour surface from algebraic equations, or from a set of numerical data related to points in space.